This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpnnen2lem11

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

Ref Expression
Hypotheses rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
rpnnen2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
rpnnen2.3 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
rpnnen2.4 ⊢ ( 𝜑 → 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) )
rpnnen2.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) )
rpnnen2.6 ⊢ ( 𝜓 ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
Assertion rpnnen2lem11 ( 𝜑 → ¬ 𝜓 )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2 rpnnen2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
3 rpnnen2.3 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
4 rpnnen2.4 ⊢ ( 𝜑 → 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) )
5 rpnnen2.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) ) )
6 rpnnen2.6 ⊢ ( 𝜓 ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
7 eldifi ⊢ ( 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑚 ∈ 𝐴 )
8 ssel2 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ ℕ )
9 7 8 sylan2 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑚 ∈ ℕ )
10 2 4 9 syl2anc ⊢ ( 𝜑 → 𝑚 ∈ ℕ )
11 1 rpnnen2lem6 ⊢ ( ( 𝐵 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
12 3 10 11 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
13 3nn ⊢ 3 ∈ ℕ
14 nnrecre ⊢ ( 3 ∈ ℕ → ( 1 / 3 ) ∈ ℝ )
15 13 14 ax-mp ⊢ ( 1 / 3 ) ∈ ℝ
16 10 nnnn0d ⊢ ( 𝜑 → 𝑚 ∈ ℕ0 )
17 reexpcl ⊢ ( ( ( 1 / 3 ) ∈ ℝ ∧ 𝑚 ∈ ℕ0 ) → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ )
18 15 16 17 sylancr ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ )
19 1 rpnnen2lem6 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
20 2 10 19 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
21 nnrp ⊢ ( 3 ∈ ℕ → 3 ∈ ℝ+ )
22 rpreccl ⊢ ( 3 ∈ ℝ+ → ( 1 / 3 ) ∈ ℝ+ )
23 13 21 22 mp2b ⊢ ( 1 / 3 ) ∈ ℝ+
24 10 nnzd ⊢ ( 𝜑 → 𝑚 ∈ ℤ )
25 rpexpcl ⊢ ( ( ( 1 / 3 ) ∈ ℝ+ ∧ 𝑚 ∈ ℤ ) → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ+ )
26 23 24 25 sylancr ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ+ )
27 26 rpred ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ )
28 27 rehalfcld ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) ∈ ℝ )
29 4 snssd ⊢ ( 𝜑 → { 𝑚 } ⊆ ( 𝐴 ∖ 𝐵 ) )
30 2 ssdifd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ( ℕ ∖ 𝐵 ) )
31 29 30 sstrd ⊢ ( 𝜑 → { 𝑚 } ⊆ ( ℕ ∖ 𝐵 ) )
32 10 snssd ⊢ ( 𝜑 → { 𝑚 } ⊆ ℕ )
33 ssconb ⊢ ( ( 𝐵 ⊆ ℕ ∧ { 𝑚 } ⊆ ℕ ) → ( 𝐵 ⊆ ( ℕ ∖ { 𝑚 } ) ↔ { 𝑚 } ⊆ ( ℕ ∖ 𝐵 ) ) )
34 3 32 33 syl2anc ⊢ ( 𝜑 → ( 𝐵 ⊆ ( ℕ ∖ { 𝑚 } ) ↔ { 𝑚 } ⊆ ( ℕ ∖ 𝐵 ) ) )
35 31 34 mpbird ⊢ ( 𝜑 → 𝐵 ⊆ ( ℕ ∖ { 𝑚 } ) )
36 difssd ⊢ ( 𝜑 → ( ℕ ∖ { 𝑚 } ) ⊆ ℕ )
37 1 rpnnen2lem7 ⊢ ( ( 𝐵 ⊆ ( ℕ ∖ { 𝑚 } ) ∧ ( ℕ ∖ { 𝑚 } ) ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑚 } ) ) ‘ 𝑘 ) )
38 35 36 10 37 syl3anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑚 } ) ) ‘ 𝑘 ) )
39 1 rpnnen2lem9 ⊢ ( 𝑚 ∈ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑚 } ) ) ‘ 𝑘 ) = ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) )
40 10 39 syl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑚 } ) ) ‘ 𝑘 ) = ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) )
41 15 recni ⊢ ( 1 / 3 ) ∈ ℂ
42 expp1 ⊢ ( ( ( 1 / 3 ) ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) · ( 1 / 3 ) ) )
43 41 16 42 sylancr ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) · ( 1 / 3 ) ) )
44 27 recnd ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ )
45 3cn ⊢ 3 ∈ ℂ
46 3ne0 ⊢ 3 ≠ 0
47 divrec ⊢ ( ( ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) · ( 1 / 3 ) ) )
48 45 46 47 mp3an23 ⊢ ( ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) · ( 1 / 3 ) ) )
49 44 48 syl ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) · ( 1 / 3 ) ) )
50 43 49 eqtr4d ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) )
51 50 oveq1d ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) = ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 1 − ( 1 / 3 ) ) ) )
52 ax-1cn ⊢ 1 ∈ ℂ
53 45 46 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
54 divsubdir ⊢ ( ( 3 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 3 − 1 ) / 3 ) = ( ( 3 / 3 ) − ( 1 / 3 ) ) )
55 45 52 53 54 mp3an ⊢ ( ( 3 − 1 ) / 3 ) = ( ( 3 / 3 ) − ( 1 / 3 ) )
56 3m1e2 ⊢ ( 3 − 1 ) = 2
57 56 oveq1i ⊢ ( ( 3 − 1 ) / 3 ) = ( 2 / 3 )
58 45 46 dividi ⊢ ( 3 / 3 ) = 1
59 58 oveq1i ⊢ ( ( 3 / 3 ) − ( 1 / 3 ) ) = ( 1 − ( 1 / 3 ) )
60 55 57 59 3eqtr3ri ⊢ ( 1 − ( 1 / 3 ) ) = ( 2 / 3 )
61 60 oveq2i ⊢ ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 1 − ( 1 / 3 ) ) ) = ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 2 / 3 ) )
62 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
63 divcan7 ⊢ ( ( ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
64 62 53 63 mp3an23 ⊢ ( ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ → ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
65 44 64 syl ⊢ ( 𝜑 → ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
66 61 65 eqtrid ⊢ ( 𝜑 → ( ( ( ( 1 / 3 ) ↑ 𝑚 ) / 3 ) / ( 1 − ( 1 / 3 ) ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
67 51 66 eqtrd ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
68 67 oveq2d ⊢ ( 𝜑 → ( 0 + ( ( ( 1 / 3 ) ↑ ( 𝑚 + 1 ) ) / ( 1 − ( 1 / 3 ) ) ) ) = ( 0 + ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) ) )
69 28 recnd ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) ∈ ℂ )
70 69 addlidd ⊢ ( 𝜑 → ( 0 + ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
71 40 68 70 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ ( ℕ ∖ { 𝑚 } ) ) ‘ 𝑘 ) = ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
72 38 71 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ≤ ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) )
73 rphalflt ⊢ ( ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℝ+ → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) < ( ( 1 / 3 ) ↑ 𝑚 ) )
74 26 73 syl ⊢ ( 𝜑 → ( ( ( 1 / 3 ) ↑ 𝑚 ) / 2 ) < ( ( 1 / 3 ) ↑ 𝑚 ) )
75 12 28 27 72 74 lelttrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) < ( ( 1 / 3 ) ↑ 𝑚 ) )
76 eluznn ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
77 10 76 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
78 1 rpnnen2lem1 ⊢ ( ( { 𝑚 } ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) = if ( 𝑘 ∈ { 𝑚 } , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
79 32 77 78 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) = if ( 𝑘 ∈ { 𝑚 } , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
80 79 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) if ( 𝑘 ∈ { 𝑚 } , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
81 uzid ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) )
82 24 81 syl ⊢ ( 𝜑 → 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) )
83 82 snssd ⊢ ( 𝜑 → { 𝑚 } ⊆ ( ℤ≥ ‘ 𝑚 ) )
84 vex ⊢ 𝑚 ∈ V
85 oveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 1 / 3 ) ↑ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑚 ) )
86 85 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℂ ↔ ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ ) )
87 84 86 ralsn ⊢ ( ∀ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℂ ↔ ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ )
88 44 87 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℂ )
89 ssidd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑚 ) )
90 89 orcd ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑚 ) ∨ ( ℤ≥ ‘ 𝑚 ) ∈ Fin ) )
91 sumss2 ⊢ ( ( ( { 𝑚 } ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∀ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℂ ) ∧ ( ( ℤ≥ ‘ 𝑚 ) ⊆ ( ℤ≥ ‘ 𝑚 ) ∨ ( ℤ≥ ‘ 𝑚 ) ∈ Fin ) ) → Σ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) if ( 𝑘 ∈ { 𝑚 } , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
92 83 88 90 91 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) if ( 𝑘 ∈ { 𝑚 } , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
93 85 sumsn ⊢ ( ( 𝑚 ∈ ℕ ∧ ( ( 1 / 3 ) ↑ 𝑚 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑚 ) )
94 10 44 93 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑚 } ( ( 1 / 3 ) ↑ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑚 ) )
95 80 92 94 3eqtr2d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) = ( ( 1 / 3 ) ↑ 𝑚 ) )
96 4 7 syl ⊢ ( 𝜑 → 𝑚 ∈ 𝐴 )
97 96 snssd ⊢ ( 𝜑 → { 𝑚 } ⊆ 𝐴 )
98 1 rpnnen2lem7 ⊢ ( ( { 𝑚 } ⊆ 𝐴 ∧ 𝐴 ⊆ ℕ ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
99 97 2 10 98 syl3anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ { 𝑚 } ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
100 95 99 eqbrtrrd ⊢ ( 𝜑 → ( ( 1 / 3 ) ↑ 𝑚 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
101 12 18 20 75 100 ltletrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) < Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
102 12 101 gtned ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ≠ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
103 1 2 3 4 5 6 rpnnen2lem10 ⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
104 103 ex ⊢ ( 𝜑 → ( 𝜓 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )
105 104 necon3ad ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ≠ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) → ¬ 𝜓 ) )
106 102 105 mpd ⊢ ( 𝜑 → ¬ 𝜓 )