# Metamath Proof Explorer

## Theorem prmreclem1

Description: Lemma for prmrec . Properties of the "square part" function, which extracts the m of the decomposition N = r m ^ 2 , with m maximal and r squarefree. (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypothesis prmreclem1.1 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
Assertion prmreclem1 ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ∈ ℕ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ∧ ( 𝐾 ∈ ( ℤ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 prmreclem1.1 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
2 ssrab2 { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℕ
3 breq2 ( 𝑛 = 𝑁 → ( ( 𝑟 ↑ 2 ) ∥ 𝑛 ↔ ( 𝑟 ↑ 2 ) ∥ 𝑁 ) )
4 3 rabbidv ( 𝑛 = 𝑁 → { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } = { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
5 4 supeq1d ( 𝑛 = 𝑁 → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
6 ltso < Or ℝ
7 6 supex sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ V
8 5 1 7 fvmpt ( 𝑁 ∈ ℕ → ( 𝑄𝑁 ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
9 nnssz ℕ ⊆ ℤ
10 2 9 sstri { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ
11 oveq1 ( 𝑟 = 1 → ( 𝑟 ↑ 2 ) = ( 1 ↑ 2 ) )
12 sq1 ( 1 ↑ 2 ) = 1
13 11 12 syl6eq ( 𝑟 = 1 → ( 𝑟 ↑ 2 ) = 1 )
14 13 breq1d ( 𝑟 = 1 → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ 1 ∥ 𝑁 ) )
15 1nn 1 ∈ ℕ
16 15 a1i ( 𝑁 ∈ ℕ → 1 ∈ ℕ )
17 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
18 1dvds ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
19 17 18 syl ( 𝑁 ∈ ℕ → 1 ∥ 𝑁 )
20 14 16 19 elrabd ( 𝑁 ∈ ℕ → 1 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
21 20 ne0d ( 𝑁 ∈ ℕ → { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ≠ ∅ )
22 nnz ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
23 zsqcl ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℤ )
24 22 23 syl ( 𝑧 ∈ ℕ → ( 𝑧 ↑ 2 ) ∈ ℤ )
25 id ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
26 dvdsle ( ( ( 𝑧 ↑ 2 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → ( 𝑧 ↑ 2 ) ≤ 𝑁 ) )
27 24 25 26 syl2anr ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → ( 𝑧 ↑ 2 ) ≤ 𝑁 ) )
28 nnlesq ( 𝑧 ∈ ℕ → 𝑧 ≤ ( 𝑧 ↑ 2 ) )
29 28 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑧 ≤ ( 𝑧 ↑ 2 ) )
30 nnre ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
31 30 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑧 ∈ ℝ )
32 31 resqcld ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑧 ↑ 2 ) ∈ ℝ )
33 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
34 33 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑁 ∈ ℝ )
35 letr ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 ↑ 2 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑧 ≤ ( 𝑧 ↑ 2 ) ∧ ( 𝑧 ↑ 2 ) ≤ 𝑁 ) → 𝑧𝑁 ) )
36 31 32 34 35 syl3anc ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ≤ ( 𝑧 ↑ 2 ) ∧ ( 𝑧 ↑ 2 ) ≤ 𝑁 ) → 𝑧𝑁 ) )
37 29 36 mpand ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑁𝑧𝑁 ) )
38 27 37 syld ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁𝑧𝑁 ) )
39 38 ralrimiva ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ ℕ ( ( 𝑧 ↑ 2 ) ∥ 𝑁𝑧𝑁 ) )
40 oveq1 ( 𝑟 = 𝑧 → ( 𝑟 ↑ 2 ) = ( 𝑧 ↑ 2 ) )
41 40 breq1d ( 𝑟 = 𝑧 → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ ( 𝑧 ↑ 2 ) ∥ 𝑁 ) )
42 41 ralrab ( ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑁 ↔ ∀ 𝑧 ∈ ℕ ( ( 𝑧 ↑ 2 ) ∥ 𝑁𝑧𝑁 ) )
43 39 42 sylibr ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑁 )
44 brralrspcev ( ( 𝑁 ∈ ℤ ∧ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑁 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑥 )
45 17 43 44 syl2anc ( 𝑁 ∈ ℕ → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑥 )
46 suprzcl2 ( ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ ∧ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑥 ) → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
47 10 21 45 46 mp3an2i ( 𝑁 ∈ ℕ → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
48 8 47 eqeltrd ( 𝑁 ∈ ℕ → ( 𝑄𝑁 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
49 2 48 sseldi ( 𝑁 ∈ ℕ → ( 𝑄𝑁 ) ∈ ℕ )
50 oveq1 ( 𝑧 = ( 𝑄𝑁 ) → ( 𝑧 ↑ 2 ) = ( ( 𝑄𝑁 ) ↑ 2 ) )
51 50 breq1d ( 𝑧 = ( 𝑄𝑁 ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 ↔ ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
52 41 cbvrabv { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } = { 𝑧 ∈ ℕ ∣ ( 𝑧 ↑ 2 ) ∥ 𝑁 }
53 51 52 elrab2 ( ( 𝑄𝑁 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ↔ ( ( 𝑄𝑁 ) ∈ ℕ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
54 48 53 sylib ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ∈ ℕ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
55 54 simprd ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 )
56 49 adantr ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( 𝑄𝑁 ) ∈ ℕ )
57 56 nncnd ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( 𝑄𝑁 ) ∈ ℂ )
58 57 mulid1d ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑄𝑁 ) · 1 ) = ( 𝑄𝑁 ) )
59 eluz2gt1 ( 𝐾 ∈ ( ℤ ‘ 2 ) → 1 < 𝐾 )
60 59 adantl ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → 1 < 𝐾 )
61 1red ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → 1 ∈ ℝ )
62 eluz2nn ( 𝐾 ∈ ( ℤ ‘ 2 ) → 𝐾 ∈ ℕ )
63 62 adantl ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → 𝐾 ∈ ℕ )
64 63 nnred ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → 𝐾 ∈ ℝ )
65 56 nnred ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( 𝑄𝑁 ) ∈ ℝ )
66 56 nngt0d ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → 0 < ( 𝑄𝑁 ) )
67 ltmul2 ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( ( 𝑄𝑁 ) ∈ ℝ ∧ 0 < ( 𝑄𝑁 ) ) ) → ( 1 < 𝐾 ↔ ( ( 𝑄𝑁 ) · 1 ) < ( ( 𝑄𝑁 ) · 𝐾 ) ) )
68 61 64 65 66 67 syl112anc ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( 1 < 𝐾 ↔ ( ( 𝑄𝑁 ) · 1 ) < ( ( 𝑄𝑁 ) · 𝐾 ) ) )
69 60 68 mpbid ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑄𝑁 ) · 1 ) < ( ( 𝑄𝑁 ) · 𝐾 ) )
70 58 69 eqbrtrrd ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( 𝑄𝑁 ) < ( ( 𝑄𝑁 ) · 𝐾 ) )
71 nnmulcl ( ( ( 𝑄𝑁 ) ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑄𝑁 ) · 𝐾 ) ∈ ℕ )
72 49 62 71 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ∈ ℕ )
73 72 nnred ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ∈ ℝ )
74 65 73 ltnled ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑄𝑁 ) < ( ( 𝑄𝑁 ) · 𝐾 ) ↔ ¬ ( ( 𝑄𝑁 ) · 𝐾 ) ≤ ( 𝑄𝑁 ) ) )
75 70 74 mpbid ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ¬ ( ( 𝑄𝑁 ) · 𝐾 ) ≤ ( 𝑄𝑁 ) )
76 45 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑥 )
77 oveq1 ( 𝑟 = ( ( 𝑄𝑁 ) · 𝐾 ) → ( 𝑟 ↑ 2 ) = ( ( ( 𝑄𝑁 ) · 𝐾 ) ↑ 2 ) )
78 77 breq1d ( 𝑟 = ( ( 𝑄𝑁 ) · 𝐾 ) → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ ( ( ( 𝑄𝑁 ) · 𝐾 ) ↑ 2 ) ∥ 𝑁 ) )
79 72 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ∈ ℕ )
80 simpr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) )
81 63 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → 𝐾 ∈ ℕ )
82 81 nnsqcld ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∈ ℕ )
83 nnz ( ( 𝐾 ↑ 2 ) ∈ ℕ → ( 𝐾 ↑ 2 ) ∈ ℤ )
84 82 83 syl ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∈ ℤ )
85 49 nnsqcld ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℕ )
86 9 85 sseldi ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℤ )
87 85 nnne0d ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ↑ 2 ) ≠ 0 )
88 dvdsval2 ( ( ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ↔ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ∈ ℤ ) )
89 86 87 17 88 syl3anc ( 𝑁 ∈ ℕ → ( ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ↔ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ∈ ℤ ) )
90 55 89 mpbid ( 𝑁 ∈ ℕ → ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ∈ ℤ )
91 90 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ∈ ℤ )
92 86 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℤ )
93 dvdscmul ( ( ( 𝐾 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℤ ) → ( ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) ) )
94 84 91 92 93 syl3anc ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) ) )
95 80 94 mpd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) )
96 57 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝑄𝑁 ) ∈ ℂ )
97 81 nncnd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → 𝐾 ∈ ℂ )
98 96 97 sqmuld ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄𝑁 ) · 𝐾 ) ↑ 2 ) = ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) )
99 98 eqcomd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) = ( ( ( 𝑄𝑁 ) · 𝐾 ) ↑ 2 ) )
100 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
101 100 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → 𝑁 ∈ ℂ )
102 85 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℕ )
103 102 nncnd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) ↑ 2 ) ∈ ℂ )
104 87 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) ↑ 2 ) ≠ 0 )
105 101 103 104 divcan2d ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) = 𝑁 )
106 95 99 105 3brtr3d ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄𝑁 ) · 𝐾 ) ↑ 2 ) ∥ 𝑁 )
107 78 79 106 elrabd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
108 suprzub ( ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧𝑥 ∧ ( ( 𝑄𝑁 ) · 𝐾 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ) → ( ( 𝑄𝑁 ) · 𝐾 ) ≤ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
109 10 76 107 108 mp3an2i ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ≤ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
110 8 ad2antrr ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( 𝑄𝑁 ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
111 109 110 breqtrrd ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄𝑁 ) · 𝐾 ) ≤ ( 𝑄𝑁 ) )
112 75 111 mtand ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 2 ) ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) )
113 112 ex ( 𝑁 ∈ ℕ → ( 𝐾 ∈ ( ℤ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) )
114 49 55 113 3jca ( 𝑁 ∈ ℕ → ( ( 𝑄𝑁 ) ∈ ℕ ∧ ( ( 𝑄𝑁 ) ↑ 2 ) ∥ 𝑁 ∧ ( 𝐾 ∈ ( ℤ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄𝑁 ) ↑ 2 ) ) ) ) )